DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2010.228

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

Authors: Matthew Hague and Anthony Widjaja To

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract

We study (collapsible) higher-order pushdown systems --- theoretically robust and well-studied models of higher-order programs --- along with their natural subclass called (collapsible) higher-order basic process algebras. We provide a comprehensive analysis of the model checking complexity of a range of both branching-time and linear-time temporal logics. We obtain tight bounds on data, expression, and combined-complexity for both (collapsible) higher-order pushdown systems and (collapsible) higher-order basic process algebra. At order-$k$, results range from polynomial to $(k+1)$-exponential time. Finally, we study (collapsible) higher-order basic process algebras as graph generators and show that they are almost as powerful as (collapsible) higher-order pushdown systems up to MSO interpretations.

Cite as

Matthew Hague and Anthony Widjaja To. The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 228-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{hague_et_al:LIPIcs.FSTTCS.2010.228,
  author =	{Hague, Matthew and To, Anthony Widjaja},
  title =	{{The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{228--239},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.228},
  URN =		{urn:nbn:de:0030-drops-28663},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.228},
  annote =	{Keywords: Higher-Order, Collapsible, Pushdown Systems, Temporal Logics, Complexity, Model Checking}
}

Search Results

Documents authored by To, Anthony Widjaja

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message